package kodkod.analysis.ast;

import java.io.PrintWriter;
import java.util.*;

import kodkod.ast.Decl;
import kodkod.ast.Formula;
import kodkod.ast.Node;
import kodkod.ast.QuantifiedFormula;
import kodkod.ast.Variable;

public class wClusteredGraph extends Graph {
	
	wGraph ast;
	
	public boolean removeIntersection = true;
	
	public wClusteredGraph(wGraph ast, boolean removeIntersection) {
		super();
		this.ast = ast;
		
		this.removeIntersection = removeIntersection;
	}
	
//	private void createEdgeWeights() {		
//		TreeSet<wNode> connections = new TreeSet<wNode>();
//		connections.addAll(ast.subsets);
//		connections.addAll(ast.equivalencies);
//		
//		for (wNode connection : connections) {			
//			TreeSet<wEdge> edges = connection.getOutgoingEdges();
//				
//			if (edges.size() < 2) continue;
//
//			TreeSet<wNode> leftNodes = ast.getClosestReachablePrimaries(edges.first().node2);
//			TreeSet<wNode> rightNodes = ast.getClosestReachablePrimaries(edges.last().node2);
//				
//			TreeSet<wNode> intersection = new TreeSet<wNode>();
//			intersection.addAll(leftNodes);
//			intersection.retainAll(rightNodes);
//			
//			if (removeIntersection) {
//				leftNodes.removeAll(intersection);
//				rightNodes.removeAll(intersection);
//			}
//			
//			double factor = connection.get(Measure.PROMINENCE) / (leftNodes.size() + rightNodes.size());
//			if (ast.equivalencies.contains(connection)) factor *= 2;
//			
//			for (wNode node1 : leftNodes) {
//				for (wNode node2 : rightNodes) if (node1 != node2) {
//					wNode newNode1 = getNode(node1.node);
//					wNode newNode2 = getNode(node2.node);
//					newNode1.measures = node1.measures;
//					newNode2.measures = node2.measures;
//					
//					wEdge edge = findEdge(newNode1, newNode2);
//					edge.weight += factor * 100;
//				}
//			}
//		}
//		
//		// add subset-relation from skolemization
//		for (wNode quantifier : ast.quantifiers) {
//			if (quantifier.getOutgoingEdges().size() < 2) continue;
//			
//			QuantifiedFormula formula = (QuantifiedFormula)quantifier.node;
//			 
//			for (Decl decl : formula.decls()) {
//				wNode variable = ast.getNode(decl.variable());
//				if (!(variable.node instanceof Variable)) continue; // because non-skolemized vars were deleted
//				TreeSet<wNode> expressions = ast.getClosestReachablePrimaries(ast.getNode(decl.expression()));
//				
//				if (expressions.size() == 0) continue;
//				
//				double factor = quantifier.get(Measure.PROMINENCE) / (expressions.size() + 1);
//				
//				for (wNode expression : expressions) {
//					wNode newNode1 = getNode(expression.node);
//					wNode newNode2 = getNode(variable.node);
//					newNode1.measures = expression.measures;
//					newNode2.measures = variable.measures;
//					
//					wEdge edge = findEdge(newNode1, newNode2);
//					edge.weight += factor * 100;
//				}
//			}
//		}
//		
//		// add joined multiplicities
//		for (wNode multiplicity : ast.multiplicities) {
//			TreeSet<wNode> expressions = ast.getClosestReachablePrimaries(multiplicity);
//			if (expressions.size() < 2) continue;
//			
//			double factor = multiplicity.get(Measure.PROMINENCE) / expressions.size();
//			
//			TreeSet<wNode> set = new TreeSet<wNode>();
//			set.addAll(expressions);
//				
//			while (set.size() > 0) {
//				wNode node1 = set.pollFirst();
//				for (wNode node2 : set) {
//					wNode newNode1 = getNode(node1.node);
//					wNode newNode2 = getNode(node2.node);
//					newNode1.measures = node1.measures;
//					newNode2.measures = node2.measures;
//					
//					wEdge edge = findEdge(newNode1, newNode2);
//					edge.weight += factor * 100;
//				}
//			}
//		}
//	}
	
	public ArrayList<TreeSet<Integer>> getClusters() {
		ArrayList<TreeSet<Integer>> clusters = new ArrayList<TreeSet<Integer>>();
		
		TreeSet<wNode> nodes = new TreeSet<wNode>();
		nodes.addAll(allNodes.keySet());
		
		while (nodes.size() > 0) {	
			TreeSet<Integer> cluster = new TreeSet<Integer>();
			wNode start = nodes.pollFirst();
			cluster.add(start.primaryIndex);
			TreeSet<wEdge> outgoing = start.getOutgoingEdges();
			TreeSet<wEdge> incoming = start.getIncomingEdges();
			while (outgoing.size() > 0 || incoming.size() > 0) {
				if (outgoing.size() > 0) {
					wEdge out = outgoing.pollFirst();
					if (cluster.add(out.node2.primaryIndex)) {
						outgoing.addAll(out.node2.getOutgoingEdges());
						incoming.addAll(out.node2.getIncomingEdges());
						nodes.remove(out.node2);
					}
				}
				if (incoming.size() > 0) {
					wEdge in = incoming.pollFirst();
					if (cluster.add(in.node1.primaryIndex)) {
						outgoing.addAll(in.node1.getOutgoingEdges());
						incoming.addAll(in.node1.getIncomingEdges());
						nodes.remove(in.node1);
					}
				}
			}
			clusters.add(cluster);
		}
		
		return clusters;
	}

	public void printInfo(PrintWriter writer) {
		for (wNode node : leafNodes) if (node.primary) {
			String label = node.getLabel();
			label = label.replaceAll("\\\\n", "");
			writer.write(label + "\n");
		}
		writer.println();
	}
	
	
	public void printGraph(PrintWriter out) { 
		out.println("digraph AST {");
		
		String label = ast.problem + " clusters ";
		if (removeIntersection) {
			label += "remove intersection";
		}
		out.println("label=\""+label+"\"");

		TreeSet<wNode> done = new TreeSet<wNode>();
		
		for (wEdge edge : allEdges) {
			wNode node = getNode(edge.node1);
			if (done.add(node)) out.println(node.toString());
			
			node = getNode(edge.node2);
			if (done.add(node)) out.println(node.toString());
			
			out.println(edge.toString());
		}
		
		out.println("}");
	}
}